Termination of the given ITRSProblem could successfully be proven:



↳ ITRS
  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

filter(x, cons(y, zs)) → if_2(isdiv(x, y), x, y, zs)
Cond_mem(TRUE, x, y, zs) → TRUE
nats(x, y) → Cond_nats1(=@z(x, y), x, y)
isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
mem(x, cons(y, zs)) → Cond_mem1(>@z(y, x), x, y, zs)
if_2(FALSE, x, y, zs) → cons(x, filter(x, zs))
if_1(TRUE, x, y, zs) → filter(x, zs)
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_nats2(TRUE, x, y) → nil
Cond_isdiv1(TRUE, x, y) → FALSE
Cond_nats1(TRUE, x, y) → cons(x, nil)
nats(x, y) → Cond_nats2(>@z(x, y), x, y)
mem(x, cons(y, zs)) → Cond_mem(=@z(x, y), x, y, zs)
mem(x, nil) → FALSE
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)
filter(x, nil) → nil
sieve(cons(x, ys)) → cons(x, sieve(filter(x, ys)))
Cond_isdiv4(TRUE, x) → TRUE
sieve(nil) → nil
isprime(x) → mem(x, primes(x))
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
filter(x, cons(y, zs)) → if_1(isdiv(x, y), x, y, zs)
Cond_mem1(TRUE, x, y, zs) → mem(x, zs)
nats(x, y) → Cond_nats(>@z(y, x), x, y)
mem(x, cons(y, zs)) → Cond_mem2(>@z(x, y), x, y, zs)
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_mem2(TRUE, x, y, zs) → mem(x, zs)
Cond_nats(TRUE, x, y) → cons(x, nats(+@z(x, 1@z), y))
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
primes(x) → sieve(nats(2@z, x))
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)

The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


Added dependency pairs

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

filter(x, cons(y, zs)) → if_2(isdiv(x, y), x, y, zs)
Cond_mem(TRUE, x, y, zs) → TRUE
nats(x, y) → Cond_nats1(=@z(x, y), x, y)
isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
mem(x, cons(y, zs)) → Cond_mem1(>@z(y, x), x, y, zs)
if_2(FALSE, x, y, zs) → cons(x, filter(x, zs))
if_1(TRUE, x, y, zs) → filter(x, zs)
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_nats2(TRUE, x, y) → nil
Cond_isdiv1(TRUE, x, y) → FALSE
Cond_nats1(TRUE, x, y) → cons(x, nil)
nats(x, y) → Cond_nats2(>@z(x, y), x, y)
mem(x, cons(y, zs)) → Cond_mem(=@z(x, y), x, y, zs)
mem(x, nil) → FALSE
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)
filter(x, nil) → nil
sieve(cons(x, ys)) → cons(x, sieve(filter(x, ys)))
Cond_isdiv4(TRUE, x) → TRUE
sieve(nil) → nil
isprime(x) → mem(x, primes(x))
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
filter(x, cons(y, zs)) → if_1(isdiv(x, y), x, y, zs)
Cond_mem1(TRUE, x, y, zs) → mem(x, zs)
nats(x, y) → Cond_nats(>@z(y, x), x, y)
mem(x, cons(y, zs)) → Cond_mem2(>@z(x, y), x, y, zs)
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_mem2(TRUE, x, y, zs) → mem(x, zs)
Cond_nats(TRUE, x, y) → cons(x, nats(+@z(x, 1@z), y))
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
primes(x) → sieve(nats(2@z, x))
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)

The integer pair graph contains the following rules and edges:

(0): IF_2(FALSE, x[0], y[0], zs[0]) → FILTER(x[0], zs[0])
(1): COND_NATS(TRUE, x[1], y[1]) → NATS(+@z(x[1], 1@z), y[1])
(2): ISDIV(x[2], y[2]) → COND_ISDIV2(>@z(0@z, y[2]), x[2], y[2])
(3): COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3]))
(4): FILTER(x[4], cons(y[4], zs[4])) → IF_1(isdiv(x[4], y[4]), x[4], y[4], zs[4])
(5): ISDIV(x[5], y[5]) → COND_ISDIV1(&&(>@z(x[5], y[5]), >@z(y[5], 0@z)), x[5], y[5])
(6): ISPRIME(x[6]) → MEM(x[6], primes(x[6]))
(7): COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7])
(8): FILTER(x[8], cons(y[8], zs[8])) → ISDIV(x[8], y[8])
(9): MEM(x[9], cons(y[9], zs[9])) → COND_MEM(=@z(x[9], y[9]), x[9], y[9], zs[9])
(10): MEM(x[10], cons(y[10], zs[10])) → COND_MEM1(>@z(y[10], x[10]), x[10], y[10], zs[10])
(11): COND_ISDIV2(TRUE, x[11], y[11]) → ISDIV(x[11], -@z(y[11]))
(12): MEM(x[12], cons(y[12], zs[12])) → COND_MEM2(>@z(x[12], y[12]), x[12], y[12], zs[12])
(13): FILTER(x[13], cons(y[13], zs[13])) → IF_2(isdiv(x[13], y[13]), x[13], y[13], zs[13])
(14): NATS(x[14], y[14]) → COND_NATS2(>@z(x[14], y[14]), x[14], y[14])
(15): IF_1(TRUE, x[15], y[15], zs[15]) → FILTER(x[15], zs[15])
(16): ISPRIME(x[16]) → PRIMES(x[16])
(17): SIEVE(cons(x[17], ys[17])) → FILTER(x[17], ys[17])
(18): COND_ISDIV3(TRUE, x[18], y[18]) → ISDIV(-@z(x[18]), y[18])
(19): PRIMES(x[19]) → NATS(2@z, x[19])
(20): ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20])
(21): COND_MEM1(TRUE, x[21], y[21], zs[21]) → MEM(x[21], zs[21])
(22): NATS(x[22], y[22]) → COND_NATS1(=@z(x[22], y[22]), x[22], y[22])
(23): ISDIV(x[23], 0@z) → COND_ISDIV4(>@z(x[23], 0@z), x[23])
(24): PRIMES(x[24]) → SIEVE(nats(2@z, x[24]))
(25): SIEVE(cons(x[25], ys[25])) → SIEVE(filter(x[25], ys[25]))
(26): NATS(x[26], y[26]) → COND_NATS(>@z(y[26], x[26]), x[26], y[26])
(27): ISDIV(x[27], y[27]) → COND_ISDIV3(>@z(0@z, x[27]), x[27], y[27])

(0) -> (4), if ((zs[0] →* cons(y[4], zs[4]))∧(x[0] →* x[4]))


(0) -> (8), if ((zs[0] →* cons(y[8], zs[8]))∧(x[0] →* x[8]))


(0) -> (13), if ((zs[0] →* cons(y[13], zs[13]))∧(x[0] →* x[13]))


(1) -> (14), if ((y[1] →* y[14])∧(+@z(x[1], 1@z) →* x[14]))


(1) -> (22), if ((y[1] →* y[22])∧(+@z(x[1], 1@z) →* x[22]))


(1) -> (26), if ((y[1] →* y[26])∧(+@z(x[1], 1@z) →* x[26]))


(2) -> (11), if ((x[2] →* x[11])∧(y[2] →* y[11])∧(>@z(0@z, y[2]) →* TRUE))


(3) -> (2), if ((+@z(-@z(x[3]), y[3]) →* y[2])∧(x[3] →* x[2]))


(3) -> (5), if ((+@z(-@z(x[3]), y[3]) →* y[5])∧(x[3] →* x[5]))


(3) -> (20), if ((+@z(-@z(x[3]), y[3]) →* y[20])∧(x[3] →* x[20]))


(3) -> (23), if ((+@z(-@z(x[3]), y[3]) →* 0@z)∧(x[3] →* x[23]))


(3) -> (27), if ((+@z(-@z(x[3]), y[3]) →* y[27])∧(x[3] →* x[27]))


(4) -> (15), if ((zs[4] →* zs[15])∧(x[4] →* x[15])∧(y[4] →* y[15])∧(isdiv(x[4], y[4]) →* TRUE))


(6) -> (9), if ((primes(x[6]) →* cons(y[9], zs[9]))∧(x[6] →* x[9]))


(6) -> (10), if ((primes(x[6]) →* cons(y[10], zs[10]))∧(x[6] →* x[10]))


(6) -> (12), if ((primes(x[6]) →* cons(y[12], zs[12]))∧(x[6] →* x[12]))


(7) -> (9), if ((zs[7] →* cons(y[9], zs[9]))∧(x[7] →* x[9]))


(7) -> (10), if ((zs[7] →* cons(y[10], zs[10]))∧(x[7] →* x[10]))


(7) -> (12), if ((zs[7] →* cons(y[12], zs[12]))∧(x[7] →* x[12]))


(8) -> (2), if ((y[8] →* y[2])∧(x[8] →* x[2]))


(8) -> (5), if ((y[8] →* y[5])∧(x[8] →* x[5]))


(8) -> (20), if ((y[8] →* y[20])∧(x[8] →* x[20]))


(8) -> (23), if ((y[8] →* 0@z)∧(x[8] →* x[23]))


(8) -> (27), if ((y[8] →* y[27])∧(x[8] →* x[27]))


(10) -> (21), if ((zs[10] →* zs[21])∧(x[10] →* x[21])∧(y[10] →* y[21])∧(>@z(y[10], x[10]) →* TRUE))


(11) -> (2), if ((-@z(y[11]) →* y[2])∧(x[11] →* x[2]))


(11) -> (5), if ((-@z(y[11]) →* y[5])∧(x[11] →* x[5]))


(11) -> (20), if ((-@z(y[11]) →* y[20])∧(x[11] →* x[20]))


(11) -> (23), if ((-@z(y[11]) →* 0@z)∧(x[11] →* x[23]))


(11) -> (27), if ((-@z(y[11]) →* y[27])∧(x[11] →* x[27]))


(12) -> (7), if ((zs[12] →* zs[7])∧(x[12] →* x[7])∧(y[12] →* y[7])∧(>@z(x[12], y[12]) →* TRUE))


(13) -> (0), if ((zs[13] →* zs[0])∧(x[13] →* x[0])∧(y[13] →* y[0])∧(isdiv(x[13], y[13]) →* FALSE))


(15) -> (4), if ((zs[15] →* cons(y[4], zs[4]))∧(x[15] →* x[4]))


(15) -> (8), if ((zs[15] →* cons(y[8], zs[8]))∧(x[15] →* x[8]))


(15) -> (13), if ((zs[15] →* cons(y[13], zs[13]))∧(x[15] →* x[13]))


(16) -> (19), if ((x[16] →* x[19]))


(16) -> (24), if ((x[16] →* x[24]))


(17) -> (4), if ((ys[17] →* cons(y[4], zs[4]))∧(x[17] →* x[4]))


(17) -> (8), if ((ys[17] →* cons(y[8], zs[8]))∧(x[17] →* x[8]))


(17) -> (13), if ((ys[17] →* cons(y[13], zs[13]))∧(x[17] →* x[13]))


(18) -> (2), if ((y[18] →* y[2])∧(-@z(x[18]) →* x[2]))


(18) -> (5), if ((y[18] →* y[5])∧(-@z(x[18]) →* x[5]))


(18) -> (20), if ((y[18] →* y[20])∧(-@z(x[18]) →* x[20]))


(18) -> (23), if ((y[18] →* 0@z)∧(-@z(x[18]) →* x[23]))


(18) -> (27), if ((y[18] →* y[27])∧(-@z(x[18]) →* x[27]))


(19) -> (14), if ((x[19] →* y[14]))


(19) -> (22), if ((x[19] →* y[22]))


(19) -> (26), if ((x[19] →* y[26]))


(20) -> (3), if ((x[20] →* x[3])∧(y[20] →* y[3])∧(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)) →* TRUE))


(21) -> (9), if ((zs[21] →* cons(y[9], zs[9]))∧(x[21] →* x[9]))


(21) -> (10), if ((zs[21] →* cons(y[10], zs[10]))∧(x[21] →* x[10]))


(21) -> (12), if ((zs[21] →* cons(y[12], zs[12]))∧(x[21] →* x[12]))


(24) -> (17), if ((nats(2@z, x[24]) →* cons(x[17], ys[17])))


(24) -> (25), if ((nats(2@z, x[24]) →* cons(x[25], ys[25])))


(25) -> (17), if ((filter(x[25], ys[25]) →* cons(x[17], ys[17])))


(25) -> (25), if ((filter(x[25], ys[25]) →* cons(x[25]a, ys[25]a)))


(26) -> (1), if ((x[26] →* x[1])∧(y[26] →* y[1])∧(>@z(y[26], x[26]) →* TRUE))


(27) -> (18), if ((x[27] →* x[18])∧(y[27] →* y[18])∧(>@z(0@z, x[27]) →* TRUE))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

filter(x, cons(y, zs)) → if_2(isdiv(x, y), x, y, zs)
nats(x, y) → Cond_nats1(=@z(x, y), x, y)
isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
if_2(FALSE, x, y, zs) → cons(x, filter(x, zs))
Cond_nats2(TRUE, x, y) → nil
Cond_isdiv1(TRUE, x, y) → FALSE
Cond_nats1(TRUE, x, y) → cons(x, nil)
nats(x, y) → Cond_nats2(>@z(x, y), x, y)
sieve(cons(x, ys)) → cons(x, sieve(filter(x, ys)))
filter(x, nil) → nil
sieve(nil) → nil
Cond_isdiv4(TRUE, x) → TRUE
filter(x, cons(y, zs)) → if_1(isdiv(x, y), x, y, zs)
if_1(TRUE, x, y, zs) → filter(x, zs)
nats(x, y) → Cond_nats(>@z(y, x), x, y)
isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_nats(TRUE, x, y) → cons(x, nats(+@z(x, 1@z), y))
primes(x) → sieve(nats(2@z, x))
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)

The integer pair graph contains the following rules and edges:

(0): IF_2(FALSE, x[0], y[0], zs[0]) → FILTER(x[0], zs[0])
(1): COND_NATS(TRUE, x[1], y[1]) → NATS(+@z(x[1], 1@z), y[1])
(2): ISDIV(x[2], y[2]) → COND_ISDIV2(>@z(0@z, y[2]), x[2], y[2])
(3): COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3]))
(4): FILTER(x[4], cons(y[4], zs[4])) → IF_1(isdiv(x[4], y[4]), x[4], y[4], zs[4])
(5): ISDIV(x[5], y[5]) → COND_ISDIV1(&&(>@z(x[5], y[5]), >@z(y[5], 0@z)), x[5], y[5])
(6): ISPRIME(x[6]) → MEM(x[6], primes(x[6]))
(7): COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7])
(8): FILTER(x[8], cons(y[8], zs[8])) → ISDIV(x[8], y[8])
(9): MEM(x[9], cons(y[9], zs[9])) → COND_MEM(=@z(x[9], y[9]), x[9], y[9], zs[9])
(10): MEM(x[10], cons(y[10], zs[10])) → COND_MEM1(>@z(y[10], x[10]), x[10], y[10], zs[10])
(11): COND_ISDIV2(TRUE, x[11], y[11]) → ISDIV(x[11], -@z(y[11]))
(12): MEM(x[12], cons(y[12], zs[12])) → COND_MEM2(>@z(x[12], y[12]), x[12], y[12], zs[12])
(13): FILTER(x[13], cons(y[13], zs[13])) → IF_2(isdiv(x[13], y[13]), x[13], y[13], zs[13])
(14): NATS(x[14], y[14]) → COND_NATS2(>@z(x[14], y[14]), x[14], y[14])
(15): IF_1(TRUE, x[15], y[15], zs[15]) → FILTER(x[15], zs[15])
(16): ISPRIME(x[16]) → PRIMES(x[16])
(17): SIEVE(cons(x[17], ys[17])) → FILTER(x[17], ys[17])
(18): COND_ISDIV3(TRUE, x[18], y[18]) → ISDIV(-@z(x[18]), y[18])
(19): PRIMES(x[19]) → NATS(2@z, x[19])
(20): ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20])
(21): COND_MEM1(TRUE, x[21], y[21], zs[21]) → MEM(x[21], zs[21])
(22): NATS(x[22], y[22]) → COND_NATS1(=@z(x[22], y[22]), x[22], y[22])
(23): ISDIV(x[23], 0@z) → COND_ISDIV4(>@z(x[23], 0@z), x[23])
(24): PRIMES(x[24]) → SIEVE(nats(2@z, x[24]))
(25): SIEVE(cons(x[25], ys[25])) → SIEVE(filter(x[25], ys[25]))
(26): NATS(x[26], y[26]) → COND_NATS(>@z(y[26], x[26]), x[26], y[26])
(27): ISDIV(x[27], y[27]) → COND_ISDIV3(>@z(0@z, x[27]), x[27], y[27])

(0) -> (4), if ((zs[0] →* cons(y[4], zs[4]))∧(x[0] →* x[4]))


(0) -> (8), if ((zs[0] →* cons(y[8], zs[8]))∧(x[0] →* x[8]))


(0) -> (13), if ((zs[0] →* cons(y[13], zs[13]))∧(x[0] →* x[13]))


(1) -> (14), if ((y[1] →* y[14])∧(+@z(x[1], 1@z) →* x[14]))


(1) -> (22), if ((y[1] →* y[22])∧(+@z(x[1], 1@z) →* x[22]))


(1) -> (26), if ((y[1] →* y[26])∧(+@z(x[1], 1@z) →* x[26]))


(2) -> (11), if ((x[2] →* x[11])∧(y[2] →* y[11])∧(>@z(0@z, y[2]) →* TRUE))


(3) -> (2), if ((+@z(-@z(x[3]), y[3]) →* y[2])∧(x[3] →* x[2]))


(3) -> (5), if ((+@z(-@z(x[3]), y[3]) →* y[5])∧(x[3] →* x[5]))


(3) -> (20), if ((+@z(-@z(x[3]), y[3]) →* y[20])∧(x[3] →* x[20]))


(3) -> (23), if ((+@z(-@z(x[3]), y[3]) →* 0@z)∧(x[3] →* x[23]))


(3) -> (27), if ((+@z(-@z(x[3]), y[3]) →* y[27])∧(x[3] →* x[27]))


(4) -> (15), if ((zs[4] →* zs[15])∧(x[4] →* x[15])∧(y[4] →* y[15])∧(isdiv(x[4], y[4]) →* TRUE))


(6) -> (9), if ((primes(x[6]) →* cons(y[9], zs[9]))∧(x[6] →* x[9]))


(6) -> (10), if ((primes(x[6]) →* cons(y[10], zs[10]))∧(x[6] →* x[10]))


(6) -> (12), if ((primes(x[6]) →* cons(y[12], zs[12]))∧(x[6] →* x[12]))


(7) -> (9), if ((zs[7] →* cons(y[9], zs[9]))∧(x[7] →* x[9]))


(7) -> (10), if ((zs[7] →* cons(y[10], zs[10]))∧(x[7] →* x[10]))


(7) -> (12), if ((zs[7] →* cons(y[12], zs[12]))∧(x[7] →* x[12]))


(8) -> (2), if ((y[8] →* y[2])∧(x[8] →* x[2]))


(8) -> (5), if ((y[8] →* y[5])∧(x[8] →* x[5]))


(8) -> (20), if ((y[8] →* y[20])∧(x[8] →* x[20]))


(8) -> (23), if ((y[8] →* 0@z)∧(x[8] →* x[23]))


(8) -> (27), if ((y[8] →* y[27])∧(x[8] →* x[27]))


(10) -> (21), if ((zs[10] →* zs[21])∧(x[10] →* x[21])∧(y[10] →* y[21])∧(>@z(y[10], x[10]) →* TRUE))


(11) -> (2), if ((-@z(y[11]) →* y[2])∧(x[11] →* x[2]))


(11) -> (5), if ((-@z(y[11]) →* y[5])∧(x[11] →* x[5]))


(11) -> (20), if ((-@z(y[11]) →* y[20])∧(x[11] →* x[20]))


(11) -> (23), if ((-@z(y[11]) →* 0@z)∧(x[11] →* x[23]))


(11) -> (27), if ((-@z(y[11]) →* y[27])∧(x[11] →* x[27]))


(12) -> (7), if ((zs[12] →* zs[7])∧(x[12] →* x[7])∧(y[12] →* y[7])∧(>@z(x[12], y[12]) →* TRUE))


(13) -> (0), if ((zs[13] →* zs[0])∧(x[13] →* x[0])∧(y[13] →* y[0])∧(isdiv(x[13], y[13]) →* FALSE))


(15) -> (4), if ((zs[15] →* cons(y[4], zs[4]))∧(x[15] →* x[4]))


(15) -> (8), if ((zs[15] →* cons(y[8], zs[8]))∧(x[15] →* x[8]))


(15) -> (13), if ((zs[15] →* cons(y[13], zs[13]))∧(x[15] →* x[13]))


(16) -> (19), if ((x[16] →* x[19]))


(16) -> (24), if ((x[16] →* x[24]))


(17) -> (4), if ((ys[17] →* cons(y[4], zs[4]))∧(x[17] →* x[4]))


(17) -> (8), if ((ys[17] →* cons(y[8], zs[8]))∧(x[17] →* x[8]))


(17) -> (13), if ((ys[17] →* cons(y[13], zs[13]))∧(x[17] →* x[13]))


(18) -> (2), if ((y[18] →* y[2])∧(-@z(x[18]) →* x[2]))


(18) -> (5), if ((y[18] →* y[5])∧(-@z(x[18]) →* x[5]))


(18) -> (20), if ((y[18] →* y[20])∧(-@z(x[18]) →* x[20]))


(18) -> (23), if ((y[18] →* 0@z)∧(-@z(x[18]) →* x[23]))


(18) -> (27), if ((y[18] →* y[27])∧(-@z(x[18]) →* x[27]))


(19) -> (14), if ((x[19] →* y[14]))


(19) -> (22), if ((x[19] →* y[22]))


(19) -> (26), if ((x[19] →* y[26]))


(20) -> (3), if ((x[20] →* x[3])∧(y[20] →* y[3])∧(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)) →* TRUE))


(21) -> (9), if ((zs[21] →* cons(y[9], zs[9]))∧(x[21] →* x[9]))


(21) -> (10), if ((zs[21] →* cons(y[10], zs[10]))∧(x[21] →* x[10]))


(21) -> (12), if ((zs[21] →* cons(y[12], zs[12]))∧(x[21] →* x[12]))


(24) -> (17), if ((nats(2@z, x[24]) →* cons(x[17], ys[17])))


(24) -> (25), if ((nats(2@z, x[24]) →* cons(x[25], ys[25])))


(25) -> (17), if ((filter(x[25], ys[25]) →* cons(x[17], ys[17])))


(25) -> (25), if ((filter(x[25], ys[25]) →* cons(x[25]a, ys[25]a)))


(26) -> (1), if ((x[26] →* x[1])∧(y[26] →* y[1])∧(>@z(y[26], x[26]) →* TRUE))


(27) -> (18), if ((x[27] →* x[18])∧(y[27] →* y[18])∧(>@z(0@z, x[27]) →* TRUE))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 5 SCCs with 11 less nodes.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

filter(x, cons(y, zs)) → if_2(isdiv(x, y), x, y, zs)
nats(x, y) → Cond_nats1(=@z(x, y), x, y)
isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
if_2(FALSE, x, y, zs) → cons(x, filter(x, zs))
Cond_nats2(TRUE, x, y) → nil
Cond_isdiv1(TRUE, x, y) → FALSE
Cond_nats1(TRUE, x, y) → cons(x, nil)
nats(x, y) → Cond_nats2(>@z(x, y), x, y)
sieve(cons(x, ys)) → cons(x, sieve(filter(x, ys)))
filter(x, nil) → nil
sieve(nil) → nil
Cond_isdiv4(TRUE, x) → TRUE
filter(x, cons(y, zs)) → if_1(isdiv(x, y), x, y, zs)
if_1(TRUE, x, y, zs) → filter(x, zs)
nats(x, y) → Cond_nats(>@z(y, x), x, y)
isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_nats(TRUE, x, y) → cons(x, nats(+@z(x, 1@z), y))
primes(x) → sieve(nats(2@z, x))
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)

The integer pair graph contains the following rules and edges:

(3): COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3]))
(20): ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20])
(11): COND_ISDIV2(TRUE, x[11], y[11]) → ISDIV(x[11], -@z(y[11]))
(2): ISDIV(x[2], y[2]) → COND_ISDIV2(>@z(0@z, y[2]), x[2], y[2])
(18): COND_ISDIV3(TRUE, x[18], y[18]) → ISDIV(-@z(x[18]), y[18])
(27): ISDIV(x[27], y[27]) → COND_ISDIV3(>@z(0@z, x[27]), x[27], y[27])

(11) -> (2), if ((-@z(y[11]) →* y[2])∧(x[11] →* x[2]))


(27) -> (18), if ((x[27] →* x[18])∧(y[27] →* y[18])∧(>@z(0@z, x[27]) →* TRUE))


(18) -> (20), if ((y[18] →* y[20])∧(-@z(x[18]) →* x[20]))


(3) -> (2), if ((+@z(-@z(x[3]), y[3]) →* y[2])∧(x[3] →* x[2]))


(2) -> (11), if ((x[2] →* x[11])∧(y[2] →* y[11])∧(>@z(0@z, y[2]) →* TRUE))


(20) -> (3), if ((x[20] →* x[3])∧(y[20] →* y[3])∧(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)) →* TRUE))


(18) -> (2), if ((y[18] →* y[2])∧(-@z(x[18]) →* x[2]))


(11) -> (20), if ((-@z(y[11]) →* y[20])∧(x[11] →* x[20]))


(3) -> (27), if ((+@z(-@z(x[3]), y[3]) →* y[27])∧(x[3] →* x[27]))


(18) -> (27), if ((y[18] →* y[27])∧(-@z(x[18]) →* x[27]))


(11) -> (27), if ((-@z(y[11]) →* y[27])∧(x[11] →* x[27]))


(3) -> (20), if ((+@z(-@z(x[3]), y[3]) →* y[20])∧(x[3] →* x[20]))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(3): COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3]))
(20): ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20])
(11): COND_ISDIV2(TRUE, x[11], y[11]) → ISDIV(x[11], -@z(y[11]))
(2): ISDIV(x[2], y[2]) → COND_ISDIV2(>@z(0@z, y[2]), x[2], y[2])
(18): COND_ISDIV3(TRUE, x[18], y[18]) → ISDIV(-@z(x[18]), y[18])
(27): ISDIV(x[27], y[27]) → COND_ISDIV3(>@z(0@z, x[27]), x[27], y[27])

(11) -> (2), if ((-@z(y[11]) →* y[2])∧(x[11] →* x[2]))


(27) -> (18), if ((x[27] →* x[18])∧(y[27] →* y[18])∧(>@z(0@z, x[27]) →* TRUE))


(18) -> (20), if ((y[18] →* y[20])∧(-@z(x[18]) →* x[20]))


(3) -> (2), if ((+@z(-@z(x[3]), y[3]) →* y[2])∧(x[3] →* x[2]))


(2) -> (11), if ((x[2] →* x[11])∧(y[2] →* y[11])∧(>@z(0@z, y[2]) →* TRUE))


(20) -> (3), if ((x[20] →* x[3])∧(y[20] →* y[3])∧(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)) →* TRUE))


(18) -> (2), if ((y[18] →* y[2])∧(-@z(x[18]) →* x[2]))


(11) -> (20), if ((-@z(y[11]) →* y[20])∧(x[11] →* x[20]))


(3) -> (27), if ((+@z(-@z(x[3]), y[3]) →* y[27])∧(x[3] →* x[27]))


(18) -> (27), if ((y[18] →* y[27])∧(-@z(x[18]) →* x[27]))


(11) -> (27), if ((-@z(y[11]) →* y[27])∧(x[11] →* x[27]))


(3) -> (20), if ((+@z(-@z(x[3]), y[3]) →* y[20])∧(x[3] →* x[20]))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3])) the following chains were created:




For Pair ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20]) the following chains were created:




For Pair COND_ISDIV2(TRUE, x[11], y[11]) → ISDIV(x[11], -@z(y[11])) the following chains were created:




For Pair ISDIV(x[2], y[2]) → COND_ISDIV2(>@z(0@z, y[2]), x[2], y[2]) the following chains were created:




For Pair COND_ISDIV3(TRUE, x[18], y[18]) → ISDIV(-@z(x[18]), y[18]) the following chains were created:




For Pair ISDIV(x[27], y[27]) → COND_ISDIV3(>@z(0@z, x[27]), x[27], y[27]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(0@z) = 0   
POL(ISDIV(x1, x2)) = -1 + (-1)x1   
POL(TRUE) = 0   
POL(&&(x1, x2)) = 0   
POL(COND_ISDIV2(x1, x2, x3)) = -1 + (-1)x2   
POL(FALSE) = 0   
POL(COND_ISDIV(x1, x2, x3)) = -1 + (-1)x2 + (-1)x1   
POL(>@z(x1, x2)) = -1   
POL(-@z(x1)) = (-1)x1   
POL(>=@z(x1, x2)) = -1   
POL(+@z(x1, x2)) = x1 + x2   
POL(COND_ISDIV3(x1, x2, x3)) = -1 + (-1)x2   
POL(undefined) = -1   

The following pairs are in P>:

COND_ISDIV3(TRUE, x[18], y[18]) → ISDIV(-@z(x[18]), y[18])

The following pairs are in Pbound:

COND_ISDIV3(TRUE, x[18], y[18]) → ISDIV(-@z(x[18]), y[18])

The following pairs are in P≥:

COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3]))
ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20])
COND_ISDIV2(TRUE, x[11], y[11]) → ISDIV(x[11], -@z(y[11]))
ISDIV(x[2], y[2]) → COND_ISDIV2(>@z(0@z, y[2]), x[2], y[2])
ISDIV(x[27], y[27]) → COND_ISDIV3(>@z(0@z, x[27]), x[27], y[27])

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(FALSE, FALSE)1 ↔ FALSE1
+@z1 ↔
&&(TRUE, TRUE)1 ↔ TRUE1
&&(FALSE, TRUE)1 ↔ FALSE1
FALSE1 → &&(TRUE, FALSE)1
-@z1 ↔


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ IDP
                        ↳ IDependencyGraphProof
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(3): COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3]))
(20): ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20])
(11): COND_ISDIV2(TRUE, x[11], y[11]) → ISDIV(x[11], -@z(y[11]))
(2): ISDIV(x[2], y[2]) → COND_ISDIV2(>@z(0@z, y[2]), x[2], y[2])
(27): ISDIV(x[27], y[27]) → COND_ISDIV3(>@z(0@z, x[27]), x[27], y[27])

(11) -> (2), if ((-@z(y[11]) →* y[2])∧(x[11] →* x[2]))


(3) -> (2), if ((+@z(-@z(x[3]), y[3]) →* y[2])∧(x[3] →* x[2]))


(2) -> (11), if ((x[2] →* x[11])∧(y[2] →* y[11])∧(>@z(0@z, y[2]) →* TRUE))


(20) -> (3), if ((x[20] →* x[3])∧(y[20] →* y[3])∧(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)) →* TRUE))


(11) -> (20), if ((-@z(y[11]) →* y[20])∧(x[11] →* x[20]))


(3) -> (27), if ((+@z(-@z(x[3]), y[3]) →* y[27])∧(x[3] →* x[27]))


(11) -> (27), if ((-@z(y[11]) →* y[27])∧(x[11] →* x[27]))


(3) -> (20), if ((+@z(-@z(x[3]), y[3]) →* y[20])∧(x[3] →* x[20]))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ IDP
                        ↳ IDependencyGraphProof
                          ↳ IDP
                            ↳ IDPNonInfProof
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(3): COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3]))
(20): ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20])
(2): ISDIV(x[2], y[2]) → COND_ISDIV2(>@z(0@z, y[2]), x[2], y[2])
(11): COND_ISDIV2(TRUE, x[11], y[11]) → ISDIV(x[11], -@z(y[11]))

(11) -> (2), if ((-@z(y[11]) →* y[2])∧(x[11] →* x[2]))


(3) -> (2), if ((+@z(-@z(x[3]), y[3]) →* y[2])∧(x[3] →* x[2]))


(2) -> (11), if ((x[2] →* x[11])∧(y[2] →* y[11])∧(>@z(0@z, y[2]) →* TRUE))


(20) -> (3), if ((x[20] →* x[3])∧(y[20] →* y[3])∧(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)) →* TRUE))


(11) -> (20), if ((-@z(y[11]) →* y[20])∧(x[11] →* x[20]))


(3) -> (20), if ((+@z(-@z(x[3]), y[3]) →* y[20])∧(x[3] →* x[20]))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3])) the following chains were created:




For Pair ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20]) the following chains were created:




For Pair ISDIV(x[2], y[2]) → COND_ISDIV2(>@z(0@z, y[2]), x[2], y[2]) the following chains were created:




For Pair COND_ISDIV2(TRUE, x[11], y[11]) → ISDIV(x[11], -@z(y[11])) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(-@z(x1)) = (-1)x1   
POL(>=@z(x1, x2)) = -1   
POL(0@z) = 0   
POL(ISDIV(x1, x2)) = -1 + x2 + (2)x1   
POL(TRUE) = 0   
POL(&&(x1, x2)) = 0   
POL(COND_ISDIV2(x1, x2, x3)) = -1 + x3 + (2)x2   
POL(+@z(x1, x2)) = x1 + x2   
POL(FALSE) = 0   
POL(COND_ISDIV(x1, x2, x3)) = -1 + x3 + (2)x2 + (2)x1   
POL(undefined) = -1   
POL(>@z(x1, x2)) = -1   

The following pairs are in P>:

COND_ISDIV2(TRUE, x[11], y[11]) → ISDIV(x[11], -@z(y[11]))

The following pairs are in Pbound:

COND_ISDIV2(TRUE, x[11], y[11]) → ISDIV(x[11], -@z(y[11]))

The following pairs are in P≥:

COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3]))
ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20])
ISDIV(x[2], y[2]) → COND_ISDIV2(>@z(0@z, y[2]), x[2], y[2])

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(FALSE, FALSE)1 ↔ FALSE1
+@z1 ↔
&&(TRUE, TRUE)1 ↔ TRUE1
&&(FALSE, TRUE)1 ↔ FALSE1
&&(TRUE, FALSE)1 ↔ FALSE1
-@z1 ↔


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ IDP
                        ↳ IDependencyGraphProof
                          ↳ IDP
                            ↳ IDPNonInfProof
                              ↳ IDP
                                ↳ IDependencyGraphProof
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(3): COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3]))
(20): ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20])
(2): ISDIV(x[2], y[2]) → COND_ISDIV2(>@z(0@z, y[2]), x[2], y[2])

(3) -> (2), if ((+@z(-@z(x[3]), y[3]) →* y[2])∧(x[3] →* x[2]))


(20) -> (3), if ((x[20] →* x[3])∧(y[20] →* y[3])∧(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)) →* TRUE))


(3) -> (20), if ((+@z(-@z(x[3]), y[3]) →* y[20])∧(x[3] →* x[20]))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ IDP
                        ↳ IDependencyGraphProof
                          ↳ IDP
                            ↳ IDPNonInfProof
                              ↳ IDP
                                ↳ IDependencyGraphProof
                                  ↳ IDP
                                    ↳ IDPNonInfProof
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(20): ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20])
(3): COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3]))

(20) -> (3), if ((x[20] →* x[3])∧(y[20] →* y[3])∧(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)) →* TRUE))


(3) -> (20), if ((+@z(-@z(x[3]), y[3]) →* y[20])∧(x[3] →* x[20]))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20]) the following chains were created:




For Pair COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3])) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(-@z(x1)) = (-1)x1   
POL(>=@z(x1, x2)) = -1   
POL(0@z) = 0   
POL(ISDIV(x1, x2)) = (2)x2   
POL(TRUE) = 2   
POL(&&(x1, x2)) = -1   
POL(+@z(x1, x2)) = x1 + x2   
POL(FALSE) = -1   
POL(COND_ISDIV(x1, x2, x3)) = -1 + (2)x3   
POL(undefined) = -1   
POL(>@z(x1, x2)) = -1   

The following pairs are in P>:

ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20])
COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3]))

The following pairs are in Pbound:

COND_ISDIV(TRUE, x[3], y[3]) → ISDIV(x[3], +@z(-@z(x[3]), y[3]))

The following pairs are in P≥:
none

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(FALSE, FALSE)1 ↔ FALSE1
+@z1 ↔
TRUE1 → &&(TRUE, TRUE)1
&&(TRUE, FALSE)1 ↔ FALSE1
&&(FALSE, TRUE)1 ↔ FALSE1
-@z1 ↔


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ IDP
                        ↳ IDependencyGraphProof
                          ↳ IDP
                            ↳ IDPNonInfProof
                              ↳ IDP
                                ↳ IDependencyGraphProof
                                  ↳ IDP
                                    ↳ IDPNonInfProof
                                      ↳ AND
                                        ↳ IDP
                                          ↳ IDependencyGraphProof
                                        ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(20): ISDIV(x[20], y[20]) → COND_ISDIV(&&(>=@z(y[20], x[20]), >@z(x[20], 0@z)), x[20], y[20])


The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ IDP
                        ↳ IDependencyGraphProof
                          ↳ IDP
                            ↳ IDPNonInfProof
                              ↳ IDP
                                ↳ IDependencyGraphProof
                                  ↳ IDP
                                    ↳ IDPNonInfProof
                                      ↳ AND
                                        ↳ IDP
                                        ↳ IDP
                                          ↳ IDependencyGraphProof
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:none

R is empty.
The integer pair graph is empty.
The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
              ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

filter(x, cons(y, zs)) → if_2(isdiv(x, y), x, y, zs)
nats(x, y) → Cond_nats1(=@z(x, y), x, y)
isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
if_2(FALSE, x, y, zs) → cons(x, filter(x, zs))
Cond_nats2(TRUE, x, y) → nil
Cond_isdiv1(TRUE, x, y) → FALSE
Cond_nats1(TRUE, x, y) → cons(x, nil)
nats(x, y) → Cond_nats2(>@z(x, y), x, y)
sieve(cons(x, ys)) → cons(x, sieve(filter(x, ys)))
filter(x, nil) → nil
sieve(nil) → nil
Cond_isdiv4(TRUE, x) → TRUE
filter(x, cons(y, zs)) → if_1(isdiv(x, y), x, y, zs)
if_1(TRUE, x, y, zs) → filter(x, zs)
nats(x, y) → Cond_nats(>@z(y, x), x, y)
isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_nats(TRUE, x, y) → cons(x, nats(+@z(x, 1@z), y))
primes(x) → sieve(nats(2@z, x))
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)

The integer pair graph contains the following rules and edges:

(15): IF_1(TRUE, x[15], y[15], zs[15]) → FILTER(x[15], zs[15])
(4): FILTER(x[4], cons(y[4], zs[4])) → IF_1(isdiv(x[4], y[4]), x[4], y[4], zs[4])
(13): FILTER(x[13], cons(y[13], zs[13])) → IF_2(isdiv(x[13], y[13]), x[13], y[13], zs[13])
(0): IF_2(FALSE, x[0], y[0], zs[0]) → FILTER(x[0], zs[0])

(15) -> (13), if ((zs[15] →* cons(y[13], zs[13]))∧(x[15] →* x[13]))


(13) -> (0), if ((zs[13] →* zs[0])∧(x[13] →* x[0])∧(y[13] →* y[0])∧(isdiv(x[13], y[13]) →* FALSE))


(4) -> (15), if ((zs[4] →* zs[15])∧(x[4] →* x[15])∧(y[4] →* y[15])∧(isdiv(x[4], y[4]) →* TRUE))


(0) -> (13), if ((zs[0] →* cons(y[13], zs[13]))∧(x[0] →* x[13]))


(15) -> (4), if ((zs[15] →* cons(y[4], zs[4]))∧(x[15] →* x[4]))


(0) -> (4), if ((zs[0] →* cons(y[4], zs[4]))∧(x[0] →* x[4]))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
              ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)
Cond_isdiv1(TRUE, x, y) → FALSE
isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_isdiv4(TRUE, x) → TRUE

The integer pair graph contains the following rules and edges:

(15): IF_1(TRUE, x[15], y[15], zs[15]) → FILTER(x[15], zs[15])
(4): FILTER(x[4], cons(y[4], zs[4])) → IF_1(isdiv(x[4], y[4]), x[4], y[4], zs[4])
(13): FILTER(x[13], cons(y[13], zs[13])) → IF_2(isdiv(x[13], y[13]), x[13], y[13], zs[13])
(0): IF_2(FALSE, x[0], y[0], zs[0]) → FILTER(x[0], zs[0])

(15) -> (13), if ((zs[15] →* cons(y[13], zs[13]))∧(x[15] →* x[13]))


(13) -> (0), if ((zs[13] →* zs[0])∧(x[13] →* x[0])∧(y[13] →* y[0])∧(isdiv(x[13], y[13]) →* FALSE))


(4) -> (15), if ((zs[4] →* zs[15])∧(x[4] →* x[15])∧(y[4] →* y[15])∧(isdiv(x[4], y[4]) →* TRUE))


(0) -> (13), if ((zs[0] →* cons(y[13], zs[13]))∧(x[0] →* x[13]))


(15) -> (4), if ((zs[15] →* cons(y[4], zs[4]))∧(x[15] →* x[4]))


(0) -> (4), if ((zs[0] →* cons(y[4], zs[4]))∧(x[0] →* x[4]))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair IF_1(TRUE, x[15], y[15], zs[15]) → FILTER(x[15], zs[15]) the following chains were created:




For Pair FILTER(x[4], cons(y[4], zs[4])) → IF_1(isdiv(x[4], y[4]), x[4], y[4], zs[4]) the following chains were created:




For Pair FILTER(x[13], cons(y[13], zs[13])) → IF_2(isdiv(x[13], y[13]), x[13], y[13], zs[13]) the following chains were created:




For Pair IF_2(FALSE, x[0], y[0], zs[0]) → FILTER(x[0], zs[0]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(IF_1(x1, x2, x3, x4)) = -1 + x4 + (-1)x2   
POL(Cond_isdiv2(x1, x2, x3)) = 3 + (3)x3   
POL(0@z) = 0   
POL(TRUE) = 0   
POL(&&(x1, x2)) = 0   
POL(Cond_isdiv4(x1, x2)) = 1 + (3)x2   
POL(IF_2(x1, x2, x3, x4)) = -1 + x4 + (-1)x2   
POL(Cond_isdiv1(x1, x2, x3)) = 3 + x3   
POL(FALSE) = 0   
POL(Cond_isdiv3(x1, x2, x3)) = 3 + x3 + (2)x2 + (3)x1   
POL(isdiv(x1, x2)) = x1   
POL(>@z(x1, x2)) = 0   
POL(cons(x1, x2)) = 2 + x2   
POL(-@z(x1)) = 0   
POL(>=@z(x1, x2)) = 0   
POL(Cond_isdiv(x1, x2, x3)) = 2   
POL(+@z(x1, x2)) = 0   
POL(undefined) = 0   
POL(FILTER(x1, x2)) = -1 + x2 + (-1)x1   

The following pairs are in P>:

FILTER(x[4], cons(y[4], zs[4])) → IF_1(isdiv(x[4], y[4]), x[4], y[4], zs[4])
FILTER(x[13], cons(y[13], zs[13])) → IF_2(isdiv(x[13], y[13]), x[13], y[13], zs[13])

The following pairs are in Pbound:

IF_1(TRUE, x[15], y[15], zs[15]) → FILTER(x[15], zs[15])
FILTER(x[4], cons(y[4], zs[4])) → IF_1(isdiv(x[4], y[4]), x[4], y[4], zs[4])
FILTER(x[13], cons(y[13], zs[13])) → IF_2(isdiv(x[13], y[13]), x[13], y[13], zs[13])
IF_2(FALSE, x[0], y[0], zs[0]) → FILTER(x[0], zs[0])

The following pairs are in P≥:

IF_1(TRUE, x[15], y[15], zs[15]) → FILTER(x[15], zs[15])
IF_2(FALSE, x[0], y[0], zs[0]) → FILTER(x[0], zs[0])

At least the following rules have been oriented under context sensitive arithmetic replacement:

+@z1 ↔
-@z1 ↔


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ AND
                        ↳ IDP
                          ↳ IDependencyGraphProof
                        ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)
Cond_isdiv1(TRUE, x, y) → FALSE
isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_isdiv4(TRUE, x) → TRUE

The integer pair graph is empty.
The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ AND
                        ↳ IDP
                        ↳ IDP
                          ↳ IDependencyGraphProof
              ↳ IDP
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)
Cond_isdiv1(TRUE, x, y) → FALSE
isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_isdiv4(TRUE, x) → TRUE

The integer pair graph contains the following rules and edges:

(15): IF_1(TRUE, x[15], y[15], zs[15]) → FILTER(x[15], zs[15])
(0): IF_2(FALSE, x[0], y[0], zs[0]) → FILTER(x[0], zs[0])


The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

filter(x, cons(y, zs)) → if_2(isdiv(x, y), x, y, zs)
nats(x, y) → Cond_nats1(=@z(x, y), x, y)
isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
if_2(FALSE, x, y, zs) → cons(x, filter(x, zs))
Cond_nats2(TRUE, x, y) → nil
Cond_isdiv1(TRUE, x, y) → FALSE
Cond_nats1(TRUE, x, y) → cons(x, nil)
nats(x, y) → Cond_nats2(>@z(x, y), x, y)
sieve(cons(x, ys)) → cons(x, sieve(filter(x, ys)))
filter(x, nil) → nil
sieve(nil) → nil
Cond_isdiv4(TRUE, x) → TRUE
filter(x, cons(y, zs)) → if_1(isdiv(x, y), x, y, zs)
if_1(TRUE, x, y, zs) → filter(x, zs)
nats(x, y) → Cond_nats(>@z(y, x), x, y)
isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_nats(TRUE, x, y) → cons(x, nats(+@z(x, 1@z), y))
primes(x) → sieve(nats(2@z, x))
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)

The integer pair graph contains the following rules and edges:

(25): SIEVE(cons(x[25], ys[25])) → SIEVE(filter(x[25], ys[25]))

(25) -> (25), if ((filter(x[25], ys[25]) →* cons(x[25]a, ys[25]a)))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)
filter(x, nil) → nil
Cond_isdiv4(TRUE, x) → TRUE
filter(x, cons(y, zs)) → if_1(isdiv(x, y), x, y, zs)
if_1(TRUE, x, y, zs) → filter(x, zs)
filter(x, cons(y, zs)) → if_2(isdiv(x, y), x, y, zs)
isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
if_2(FALSE, x, y, zs) → cons(x, filter(x, zs))
Cond_isdiv1(TRUE, x, y) → FALSE

The integer pair graph contains the following rules and edges:

(25): SIEVE(cons(x[25], ys[25])) → SIEVE(filter(x[25], ys[25]))

(25) -> (25), if ((filter(x[25], ys[25]) →* cons(x[25]a, ys[25]a)))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair SIEVE(cons(x[25], ys[25])) → SIEVE(filter(x[25], ys[25])) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(SIEVE(x1)) = -1 + x1   
POL(Cond_isdiv2(x1, x2, x3)) = 0   
POL(0@z) = 0   
POL(TRUE) = 0   
POL(&&(x1, x2)) = 0   
POL(Cond_isdiv4(x1, x2)) = 0   
POL(Cond_isdiv1(x1, x2, x3)) = 0   
POL(if_1(x1, x2, x3, x4)) = x4 + (2)x1   
POL(FALSE) = 0   
POL(Cond_isdiv3(x1, x2, x3)) = 0   
POL(if_2(x1, x2, x3, x4)) = 1 + x4 + x1   
POL(>@z(x1, x2)) = 0   
POL(isdiv(x1, x2)) = 0   
POL(cons(x1, x2)) = 1 + x2   
POL(-@z(x1)) = 0   
POL(>=@z(x1, x2)) = 0   
POL(Cond_isdiv(x1, x2, x3)) = 0   
POL(filter(x1, x2)) = x2   
POL(+@z(x1, x2)) = 0   
POL(nil) = 0   
POL(undefined) = 0   

The following pairs are in P>:

SIEVE(cons(x[25], ys[25])) → SIEVE(filter(x[25], ys[25]))

The following pairs are in Pbound:

SIEVE(cons(x[25], ys[25])) → SIEVE(filter(x[25], ys[25]))

The following pairs are in P≥:
none

At least the following rules have been oriented under context sensitive arithmetic replacement:

filter(x, cons(y, zs))1 ↔ if_2(isdiv(x, y), x, y, zs)1
isdiv(x, 0@z)1 ↔ Cond_isdiv4(>@z(x, 0@z), x)1
Cond_isdiv2(TRUE, x, y)1 ↔ isdiv(x, -@z(y))1
filter(x, cons(y, zs))1 → if_1(isdiv(x, y), x, y, zs)1
&&(FALSE, TRUE)1 ↔ FALSE1
if_2(FALSE, x, y, zs)1 → cons(x, filter(x, zs))1
&&(TRUE, FALSE)1 ↔ FALSE1
if_1(TRUE, x, y, zs)1 → filter(x, zs)1
isdiv(x, y)1 ↔ Cond_isdiv2(>@z(0@z, y), x, y)1
Cond_isdiv(TRUE, x, y)1 ↔ isdiv(x, +@z(-@z(x), y))1
&&(FALSE, FALSE)1 ↔ FALSE1
isdiv(x, y)1 ↔ Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)1
Cond_isdiv1(TRUE, x, y)1 ↔ FALSE1
isdiv(x, y)1 ↔ Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)1
isdiv(x, y)1 ↔ Cond_isdiv3(>@z(0@z, x), x, y)1
filter(x, nil)1 → nil1
&&(TRUE, TRUE)1 ↔ TRUE1
+@z1 ↔
-@z1 ↔
Cond_isdiv3(TRUE, x, y)1 ↔ isdiv(-@z(x), y)1
Cond_isdiv4(TRUE, x)1 ↔ TRUE1


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ IDP
                        ↳ IDependencyGraphProof
              ↳ IDP
              ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)
filter(x, nil) → nil
Cond_isdiv4(TRUE, x) → TRUE
filter(x, cons(y, zs)) → if_1(isdiv(x, y), x, y, zs)
if_1(TRUE, x, y, zs) → filter(x, zs)
filter(x, cons(y, zs)) → if_2(isdiv(x, y), x, y, zs)
isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
if_2(FALSE, x, y, zs) → cons(x, filter(x, zs))
Cond_isdiv1(TRUE, x, y) → FALSE

The integer pair graph is empty.
The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
              ↳ IDP

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

filter(x, cons(y, zs)) → if_2(isdiv(x, y), x, y, zs)
nats(x, y) → Cond_nats1(=@z(x, y), x, y)
isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
if_2(FALSE, x, y, zs) → cons(x, filter(x, zs))
Cond_nats2(TRUE, x, y) → nil
Cond_isdiv1(TRUE, x, y) → FALSE
Cond_nats1(TRUE, x, y) → cons(x, nil)
nats(x, y) → Cond_nats2(>@z(x, y), x, y)
sieve(cons(x, ys)) → cons(x, sieve(filter(x, ys)))
filter(x, nil) → nil
sieve(nil) → nil
Cond_isdiv4(TRUE, x) → TRUE
filter(x, cons(y, zs)) → if_1(isdiv(x, y), x, y, zs)
if_1(TRUE, x, y, zs) → filter(x, zs)
nats(x, y) → Cond_nats(>@z(y, x), x, y)
isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_nats(TRUE, x, y) → cons(x, nats(+@z(x, 1@z), y))
primes(x) → sieve(nats(2@z, x))
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)

The integer pair graph contains the following rules and edges:

(1): COND_NATS(TRUE, x[1], y[1]) → NATS(+@z(x[1], 1@z), y[1])
(26): NATS(x[26], y[26]) → COND_NATS(>@z(y[26], x[26]), x[26], y[26])

(26) -> (1), if ((x[26] →* x[1])∧(y[26] →* y[1])∧(>@z(y[26], x[26]) →* TRUE))


(1) -> (26), if ((y[1] →* y[26])∧(+@z(x[1], 1@z) →* x[26]))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(1): COND_NATS(TRUE, x[1], y[1]) → NATS(+@z(x[1], 1@z), y[1])
(26): NATS(x[26], y[26]) → COND_NATS(>@z(y[26], x[26]), x[26], y[26])

(26) -> (1), if ((x[26] →* x[1])∧(y[26] →* y[1])∧(>@z(y[26], x[26]) →* TRUE))


(1) -> (26), if ((y[1] →* y[26])∧(+@z(x[1], 1@z) →* x[26]))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_NATS(TRUE, x[1], y[1]) → NATS(+@z(x[1], 1@z), y[1]) the following chains were created:




For Pair NATS(x[26], y[26]) → COND_NATS(>@z(y[26], x[26]), x[26], y[26]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = -1   
POL(COND_NATS(x1, x2, x3)) = -1 + x3 + (-1)x2   
POL(+@z(x1, x2)) = x1 + x2   
POL(NATS(x1, x2)) = -1 + x2 + (-1)x1   
POL(FALSE) = -1   
POL(1@z) = 1   
POL(undefined) = -1   
POL(>@z(x1, x2)) = -1   

The following pairs are in P>:

COND_NATS(TRUE, x[1], y[1]) → NATS(+@z(x[1], 1@z), y[1])

The following pairs are in Pbound:

COND_NATS(TRUE, x[1], y[1]) → NATS(+@z(x[1], 1@z), y[1])

The following pairs are in P≥:

NATS(x[26], y[26]) → COND_NATS(>@z(y[26], x[26]), x[26], y[26])

At least the following rules have been oriented under context sensitive arithmetic replacement:

+@z1 ↔


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ IDP
                        ↳ IDependencyGraphProof
              ↳ IDP

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(26): NATS(x[26], y[26]) → COND_NATS(>@z(y[26], x[26]), x[26], y[26])


The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

filter(x, cons(y, zs)) → if_2(isdiv(x, y), x, y, zs)
nats(x, y) → Cond_nats1(=@z(x, y), x, y)
isdiv(x, 0@z) → Cond_isdiv4(>@z(x, 0@z), x)
if_2(FALSE, x, y, zs) → cons(x, filter(x, zs))
Cond_nats2(TRUE, x, y) → nil
Cond_isdiv1(TRUE, x, y) → FALSE
Cond_nats1(TRUE, x, y) → cons(x, nil)
nats(x, y) → Cond_nats2(>@z(x, y), x, y)
sieve(cons(x, ys)) → cons(x, sieve(filter(x, ys)))
filter(x, nil) → nil
sieve(nil) → nil
Cond_isdiv4(TRUE, x) → TRUE
filter(x, cons(y, zs)) → if_1(isdiv(x, y), x, y, zs)
if_1(TRUE, x, y, zs) → filter(x, zs)
nats(x, y) → Cond_nats(>@z(y, x), x, y)
isdiv(x, y) → Cond_isdiv1(&&(>@z(x, y), >@z(y, 0@z)), x, y)
Cond_nats(TRUE, x, y) → cons(x, nats(+@z(x, 1@z), y))
primes(x) → sieve(nats(2@z, x))
Cond_isdiv(TRUE, x, y) → isdiv(x, +@z(-@z(x), y))
isdiv(x, y) → Cond_isdiv2(>@z(0@z, y), x, y)
Cond_isdiv3(TRUE, x, y) → isdiv(-@z(x), y)
isdiv(x, y) → Cond_isdiv(&&(>=@z(y, x), >@z(x, 0@z)), x, y)
Cond_isdiv2(TRUE, x, y) → isdiv(x, -@z(y))
isdiv(x, y) → Cond_isdiv3(>@z(0@z, x), x, y)

The integer pair graph contains the following rules and edges:

(21): COND_MEM1(TRUE, x[21], y[21], zs[21]) → MEM(x[21], zs[21])
(10): MEM(x[10], cons(y[10], zs[10])) → COND_MEM1(>@z(y[10], x[10]), x[10], y[10], zs[10])
(12): MEM(x[12], cons(y[12], zs[12])) → COND_MEM2(>@z(x[12], y[12]), x[12], y[12], zs[12])
(7): COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7])

(10) -> (21), if ((zs[10] →* zs[21])∧(x[10] →* x[21])∧(y[10] →* y[21])∧(>@z(y[10], x[10]) →* TRUE))


(21) -> (12), if ((zs[21] →* cons(y[12], zs[12]))∧(x[21] →* x[12]))


(7) -> (10), if ((zs[7] →* cons(y[10], zs[10]))∧(x[7] →* x[10]))


(7) -> (12), if ((zs[7] →* cons(y[12], zs[12]))∧(x[7] →* x[12]))


(21) -> (10), if ((zs[21] →* cons(y[10], zs[10]))∧(x[21] →* x[10]))


(12) -> (7), if ((zs[12] →* zs[7])∧(x[12] →* x[7])∧(y[12] →* y[7])∧(>@z(x[12], y[12]) →* TRUE))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(21): COND_MEM1(TRUE, x[21], y[21], zs[21]) → MEM(x[21], zs[21])
(10): MEM(x[10], cons(y[10], zs[10])) → COND_MEM1(>@z(y[10], x[10]), x[10], y[10], zs[10])
(12): MEM(x[12], cons(y[12], zs[12])) → COND_MEM2(>@z(x[12], y[12]), x[12], y[12], zs[12])
(7): COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7])

(10) -> (21), if ((zs[10] →* zs[21])∧(x[10] →* x[21])∧(y[10] →* y[21])∧(>@z(y[10], x[10]) →* TRUE))


(21) -> (12), if ((zs[21] →* cons(y[12], zs[12]))∧(x[21] →* x[12]))


(7) -> (10), if ((zs[7] →* cons(y[10], zs[10]))∧(x[7] →* x[10]))


(7) -> (12), if ((zs[7] →* cons(y[12], zs[12]))∧(x[7] →* x[12]))


(21) -> (10), if ((zs[21] →* cons(y[10], zs[10]))∧(x[21] →* x[10]))


(12) -> (7), if ((zs[12] →* zs[7])∧(x[12] →* x[7])∧(y[12] →* y[7])∧(>@z(x[12], y[12]) →* TRUE))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_MEM1(TRUE, x[21], y[21], zs[21]) → MEM(x[21], zs[21]) the following chains were created:




For Pair MEM(x[10], cons(y[10], zs[10])) → COND_MEM1(>@z(y[10], x[10]), x[10], y[10], zs[10]) the following chains were created:




For Pair MEM(x[12], cons(y[12], zs[12])) → COND_MEM2(>@z(x[12], y[12]), x[12], y[12], zs[12]) the following chains were created:




For Pair COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(cons(x1, x2)) = 2 + x2   
POL(COND_MEM2(x1, x2, x3, x4)) = -1 + (2)x4 + (-1)x2   
POL(MEM(x1, x2)) = -1 + (2)x2 + (-1)x1   
POL(TRUE) = 0   
POL(FALSE) = 0   
POL(undefined) = 0   
POL(>@z(x1, x2)) = 0   
POL(COND_MEM1(x1, x2, x3, x4)) = 1 + (2)x4 + (-1)x2   

The following pairs are in P>:

COND_MEM1(TRUE, x[21], y[21], zs[21]) → MEM(x[21], zs[21])

The following pairs are in Pbound:

COND_MEM1(TRUE, x[21], y[21], zs[21]) → MEM(x[21], zs[21])
MEM(x[10], cons(y[10], zs[10])) → COND_MEM1(>@z(y[10], x[10]), x[10], y[10], zs[10])
MEM(x[12], cons(y[12], zs[12])) → COND_MEM2(>@z(x[12], y[12]), x[12], y[12], zs[12])
COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7])

The following pairs are in P≥:

MEM(x[10], cons(y[10], zs[10])) → COND_MEM1(>@z(y[10], x[10]), x[10], y[10], zs[10])
MEM(x[12], cons(y[12], zs[12])) → COND_MEM2(>@z(x[12], y[12]), x[12], y[12], zs[12])
COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7])

There are no usable rules.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ AND
                        ↳ IDP
                          ↳ IDependencyGraphProof
                        ↳ IDP

I DP problem:
The following domains are used:none

R is empty.
The integer pair graph is empty.
The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ AND
                        ↳ IDP
                        ↳ IDP
                          ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(10): MEM(x[10], cons(y[10], zs[10])) → COND_MEM1(>@z(y[10], x[10]), x[10], y[10], zs[10])
(12): MEM(x[12], cons(y[12], zs[12])) → COND_MEM2(>@z(x[12], y[12]), x[12], y[12], zs[12])
(7): COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7])

(7) -> (10), if ((zs[7] →* cons(y[10], zs[10]))∧(x[7] →* x[10]))


(7) -> (12), if ((zs[7] →* cons(y[12], zs[12]))∧(x[7] →* x[12]))


(12) -> (7), if ((zs[12] →* zs[7])∧(x[12] →* x[7])∧(y[12] →* y[7])∧(>@z(x[12], y[12]) →* TRUE))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ AND
                        ↳ IDP
                        ↳ IDP
                          ↳ IDependencyGraphProof
                            ↳ IDP
                              ↳ IDPNonInfProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(7): COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7])
(12): MEM(x[12], cons(y[12], zs[12])) → COND_MEM2(>@z(x[12], y[12]), x[12], y[12], zs[12])

(7) -> (12), if ((zs[7] →* cons(y[12], zs[12]))∧(x[7] →* x[12]))


(12) -> (7), if ((zs[12] →* zs[7])∧(x[12] →* x[7])∧(y[12] →* y[7])∧(>@z(x[12], y[12]) →* TRUE))



The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7]) the following chains were created:




For Pair MEM(x[12], cons(y[12], zs[12])) → COND_MEM2(>@z(x[12], y[12]), x[12], y[12], zs[12]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(cons(x1, x2)) = 2 + x2   
POL(COND_MEM2(x1, x2, x3, x4)) = -1 + x4 + (-1)x2   
POL(MEM(x1, x2)) = -1 + x2 + (-1)x1   
POL(TRUE) = 0   
POL(FALSE) = 0   
POL(undefined) = 0   
POL(>@z(x1, x2)) = 0   

The following pairs are in P>:

MEM(x[12], cons(y[12], zs[12])) → COND_MEM2(>@z(x[12], y[12]), x[12], y[12], zs[12])

The following pairs are in Pbound:

COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7])
MEM(x[12], cons(y[12], zs[12])) → COND_MEM2(>@z(x[12], y[12]), x[12], y[12], zs[12])

The following pairs are in P≥:

COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7])

There are no usable rules.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ AND
                        ↳ IDP
                        ↳ IDP
                          ↳ IDependencyGraphProof
                            ↳ IDP
                              ↳ IDPNonInfProof
                                ↳ AND
                                  ↳ IDP
                                    ↳ IDependencyGraphProof
                                  ↳ IDP

I DP problem:
The following domains are used:none

R is empty.
The integer pair graph is empty.
The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ AND
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
              ↳ IDP
                ↳ UsableRulesProof
                  ↳ IDP
                    ↳ IDPNonInfProof
                      ↳ AND
                        ↳ IDP
                        ↳ IDP
                          ↳ IDependencyGraphProof
                            ↳ IDP
                              ↳ IDPNonInfProof
                                ↳ AND
                                  ↳ IDP
                                  ↳ IDP
                                    ↳ IDependencyGraphProof

I DP problem:
The following domains are used:none

R is empty.
The integer pair graph contains the following rules and edges:

(7): COND_MEM2(TRUE, x[7], y[7], zs[7]) → MEM(x[7], zs[7])


The set Q consists of the following terms:

filter(x0, cons(x1, x2))
Cond_mem(TRUE, x0, x1, x2)
nats(x0, x1)
mem(x0, cons(x1, x2))
if_2(FALSE, x0, x1, x2)
if_1(TRUE, x0, x1, x2)
isdiv(x0, x1)
Cond_nats2(TRUE, x0, x1)
Cond_isdiv1(TRUE, x0, x1)
Cond_nats1(TRUE, x0, x1)
mem(x0, nil)
filter(x0, nil)
sieve(cons(x0, x1))
Cond_isdiv4(TRUE, x0)
sieve(nil)
isprime(x0)
Cond_isdiv2(TRUE, x0, x1)
Cond_mem1(TRUE, x0, x1, x2)
Cond_isdiv(TRUE, x0, x1)
Cond_mem2(TRUE, x0, x1, x2)
Cond_nats(TRUE, x0, x1)
primes(x0)
Cond_isdiv3(TRUE, x0, x1)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.